Inference at * 1 0 
Iof proof for Lemma nat ind:



1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. j : 
  P(j) 

latex

 by (%S% \p.AbSetHD (get_int_arg `hn` p) p) 

latex

 1: 

 1: 4. j : 
 1: 5. j  0 
 1:   P(j)
 .

Definitions	, f(a), s = t, n - m, P  Q, , #$n, x(s), , x:AB(x), A  B, {x:A| B(x)} , x:A. B(x), i  j , t  T,
Lemmas	nat properties